\documentclass{article}

% The following \documentclass options may be useful:
%
% 10pt          To set in 10-point type instead of 9-point.
% 11pt          To set in 11-point type instead of 9-point.
% authoryear    To obtain author/year citation style instead of numeric.
\usepackage{manfnt}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb} 
\usepackage{graphicx}
\usepackage{amsmath}
\usepackage{proof}
\usepackage{hyperref}
\newcommand{\selfstar}[0]{$\mathsf{Selfstar}\ $} 
\newcommand{\cc}[0]{$\mathsf{CoC}\ $} 
\begin{document}

%% \conferenceinfo{WXYZ '05}{date, City.} 
%% \copyrightyear{2005} 
%% \copyrightdata{[to be supplied]} 

%% \titlebanner{banner above paper title}        % These are ignored unless
%% \preprintfooter{short description of paper}   % 'preprint' option specified.

\begin{center}
{\Large{Dependent Lambda Encoding with Self Types}}

\

Peng Fu, Aaron Stump

Computer Science, The University of Iowa
\end{center}

%% \title{Dependent Lambda Encoding with Self Types}
%%\subtitle{Extended Abstract}

%% \authorinfo
%%            {Peng Fu}

%% \author{Peng Fu  Aaron Stump \\
%% Computer Science, The University of Iowa}

%% \date{}
%% \maketitle  \thispagestyle{empty}

%% \begin{abstract}
%% We introduce \selfstar, a Curry-style dependent type
%% system featuring new type assignment rules for the type $\iota x.T$, 
%% together with mutual recursive definitions and the $*:*$ discipline. 
%% Standard datatype and indexed datatype can be Church- and Scott-encoded
%% as terms in \selfstar, with corresponding induction and case analysis schemes.

%% \end{abstract}

%% \category{CR-number}{subcategory}{third-level}

%% \terms
%% term1, term2

%% \keywords
%%  Lambda Encoding, Dependent Type, Type preservaiton, Progress, Confluence

%% \section{Introduction} 
%% \label{sec:intro}
%% \section{Lambda Encodings}
It is well known that natural numbers can be encoded as lambda terms using
Church encoding \cite{Church:1985} or Scott encoding (reported in \cite{CHS:72}).  So operations such as plus, 
multiplication can be performed by beta-reduction
 on lambda terms. Other inductive data structures such as trees, lists, etc. (\cite{Barendregt:97}, chapter 11 in \cite{Girard:1989})
can also be represented in a similar fashion. 

Church-encoded data can be typed in system \textbf{F} \cite{Girard:72}. But this approach is rarely adopted in dependent type systems. As summarized by Werner \cite{Werner:92}, it is inefficient to define certain operation on Church-encoded data, e.g. the predecessor function; the induction principle is not derivable and  $0 \not = 1$ cannot be proved. Thus we are led to the consideration of extending the Calculus of Construction(\cc) \cite{Coquand:1988} with inductive datatypes \cite{Paulin:1993}.

%% Scott encoding does not suffer the ineffeciency problem arised in Church encoding. But in order to define recursive functions on Scott numerals, one need either the fixpoint operator or some form of self-application(as reported in \cite{Jansen:2011}). So it seems that Scott numerals can hardly fit into a total intuitionistic type theory. \footnote{Scott numerals was claimed to be typable in System \textbf{F} \cite{Abadi:93}}

%% \section{Induction Principle}
In \cc \`a la Curry, we define $ \mathsf{Nat} := \forall X.(X \to X) \to X \to X$. One can obtain a notion of \textit{indexed iterator} by defining $\mathsf{It} := \lambda x.\lambda f.\lambda a. x f a$ and $\mathsf{It}: \forall X.\Pi x:\mathsf{Nat}. (X \to X) \to X \to X$. Thus we have 
 $\mathsf{It}\ \bar{n} =_{\beta} \lambda f.\lambda a. \bar{n}\ f\ a =_{\beta}\lambda f.\lambda a. \underbrace{f ( f ( f...(f}_{n} a)...))$. 

An indexed iterator is nice, but one may want to know if we can obtain a finer version, namely, the induction principle $\mathsf{Id}$ such that:

$\mathsf{Id} :\forall P:\mathsf{Nat} \to *. \Pi x:\mathsf{Nat}. (\Pi y:\mathsf{Nat}.(P y \to P(\mathsf{S} y))) \to P\ \bar{0} \to P\ x$ 

\noindent Let us try to construct such an $\mathsf{Id}$. First observe the following beta equalities:

$\mathsf{Id} \ \bar{0} =_{\beta} \lambda f.\lambda a.a$

$\mathsf{Id} \ \bar{n} =_{\beta} \lambda f.\lambda a.\underbrace{f\ \overline{n-1} (... f\ \bar{1}\ (f}_{n>0}\ \bar{0}\ a))$.

with $f:\Pi y:\mathsf{Nat}.(P y \to P(\mathsf{S} y)), a: P\ \bar{0}$.

\noindent So the above equalities suggest $\mathsf{Id} := \lambda x.\lambda f.\lambda a.x\ f\ a$, 
with a different notion of lambda numerals, i.e. 

$\bar{0}:= \lambda s.\lambda z.z$

$\bar{n}:= \lambda s.\lambda z.s\ \overline{n-1}\ (\overline{n-1}\ s\ z)$. 

\noindent Now let us try to type these 
lambda numerals. It is reasonable to assign $s:\Pi y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y))$
and $z: P\ \bar{0}$. Thus we have the following typing relation: 

$\bar{0} : \Pi y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y)) \to P\ \bar{0} \to P\ \bar{0}$

$\bar{1} : \Pi y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y)) \to P\ \bar{0} \to P\ \bar{1}$

$\bar{n} : \Pi y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y)) \to P\ \bar{0} \to P\ \bar{n}$

\noindent So we are led to define 

$\mathsf{Nat} := \Pi y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y)) \to P\ \bar{0} \to P\ \bar{n}$ for any $\bar{n}$. 

\noindent Two problems arise with this scheme of encoding. The first problem involves mutual recursion. The definiens of $\mathsf{Nat}$ contains $\mathsf{Nat}$ and $\mathsf{S}, \bar{0}$, while the type of $\mathsf{S}$ is $\mathsf{Nat} \to \mathsf{Nat}$ and the type of $\bar{0}$ is $\mathsf{Nat}$. This problem can be addressed by adopting mutually recursive definitions. The second problem is about quantification. We want to define a type $\mathsf{Nat}$ for any $\bar{n}$, but right now what we really have is one $\mathsf{Nat}$ for each numerals $\bar{n}$. 
We aims to solve this problem by introducing a new type construct $\iota x.T$ called \textit{self type}. The idea is that the $\iota x.T$ allows $T$ to refer, via bound variable $x$, to the term which the self type is typing. Thus we define

\noindent $\mathsf{Nat} := \iota x.\Pi y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y)) \to P\ \bar{0} \to P\ x$. The self type can only be instantiated/generalized by its own subject, so we add the following two rules and the judgement:
\[
\begin{array}{ccc}
  \infer[\textit{SelfGen}]{\Gamma \vdash t: \iota x.T}{\Gamma \vdash t: [t/x]T}
&
 \infer[\textit{SelfInst}]{\Gamma \vdash t: [t/x]T}{\Gamma \vdash t: \iota x.T}

&
\infer{\bar{n}: \iota x.\Pi y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y)) \to P\ \bar{0} \to P\ x}{\bar{n} : \Pi y:\mathsf{Nat}.(P\ y \to P(\mathsf{S}\ y)) \to P\ \bar{0} \to P\ \bar{n}}   

\\
\end{array}
\]




%% \section{Summary}

In this talk, we will introduce a type system called \selfstar with mutually recursive definitions, self types, and $*:*$. We will see how standard Church- and Scott-encoded datatype can be presented in \selfstar.

%% as terms in \selfstar, with corresponding induction and case analysis schemes.

%% We have glimpsed that induction principle can be recovered in \selfstar at the present of 
%% self type, mutual recursive definitions. We also add $*:*$ for type-level computation and excluding the needs for multi-level data type.
%% This is make \selfstar a powerful and yet somewhat simple as a full fledged dependent typed
%% programming language.


%% The present of mutual recursive definitions and $*:*$ are more than enough to depart from
%% the Curry-Howard correspondence. We want to argue that recursive definitions 
%% are there only for defining datatype like $\mathsf{Nat}$. If we 
%% want a total type theory, we can abandon $*:*$ and erase the system to $\mathbf{F}_{\omega}$, 
%% thus normalization is concluded. 


%% \subsection{Overveiw}
%% We propose a novel type system called $\mathsf{Selfstar}$, which not only enable us to type Scott encoding and Church encoding data, but also allow us to derive corresponding induction principle and case analysis principle. This makes it a possible candidate for as core functional language.  

%% Definitions of abstract reduction system, lambda calculus, simple types are given in section \ref{Pre}. We present Scott and Church numerals in both untype and typed forms in section \ref{Types}. Dependent type system and the related problem with Church encoding are discussed in detail in section \ref{Dep}. Seciton \ref{Conf}, several methods to show \textit{confluence} are given. We give an outline of proving confluence for the term system of $\mathsf{Selfstar}$ (Section \ref{Local}). Relation of confluence to type preservation is discussed in Section \ref{Conf:Presv}.  We present system $\mathsf{Selfstar}$ (Section \ref{Self}), which not only enable us to type Scott encoding and Church encoding data, but also allow us to derive corresponding induction principle and case analysis principle. 





%% \acks

%% Acknowledgments, if needed.

% We recommend abbrvnat bibliography style.

\bibliographystyle{plain}

% The bibliography should be embedded for final submission.
\bibliography{talk-prop}
%% \begin{thebibliography}{}
%% \softraggedright

%% \bibitem[Smith et~al.(2009)Smith, Jones]{smith02}
%% P. Q. Smith, and X. Y. Jones. ...reference text...

%% \end{thebibliography}

\end{document}
